Nuprl Lemma : R-compat-restrict
11,40
postcript
pdf
A
,
B
:Realizer.
A
|R-names(
B
) ||
B
|R-names(
A
)
A
||
B
latex
Definitions
x
L
.
P
(
x
)
,
A
B
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
{
T
}
,
Lemmas
R-restrict
functionality
,
l
member
wf
,
member-intersection
,
R-sub-self
,
es
realizer
wf
,
R-names
wf
,
R-compat
wf
,
maname-deq
wf
,
MaName
wf
,
l
intersection
wf
,
R-restrict
wf
,
R-compat-sub
,
R-restrict-compat
origin
A, B:Realizer. A|R-names(B) || B|R-names(A) 
A || B A, B:Realizer. A|R-names(B) || B|R-names(A) A || B x
L. P(x)
B T Qx:A. B(x)
Q